The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f(x, c(x), c(y)) → f(y, y, f(y, x, y))
f(s(x), y, z) → f(x, s(c(y)), c(z))
f(c(x), x, y) → c(y)
g(x, y) → x
g(x, y) → y

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))

S tuples:

F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1))
F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))

K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c1, c2

(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(z0, c(z0), c(z1)) → c1(F(z1, z1, f(z1, z0, z1)), F(z1, z0, z1)) by

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))

S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))
F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))

K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c2, c1

(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 1 of 4 dangling nodes:

F(z0, c(z0), c(c(z0))) → c1(F(c(z0), c(z0), c(c(z0))), F(c(z0), z0, c(z0)))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))

S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c1(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))), F(s(z0), z1, s(z0)))

K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c2, c1

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))

S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(z1), f(z1, z1, f(z1, c(z1), z1))), F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))

K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c3

(9) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))

S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))

K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c1

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))

We considered the (Usable) Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)

And the Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x₁, x₂, x₃)) = [2]x₂   
POL(c(x₁)) = [2] + x₁   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(f(x₁, x₂, x₃)) = [3] + [2]x₁ + [5]x₂   
POL(s(x₁)) = 0   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))

S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))

K tuples:

F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))

Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c1

(13) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))

S tuples:

F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2)))

K tuples:

F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))

Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c1

(15) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(s(z0), z1, z2) → c2(F(z0, s(c(z1)), c(z2))) by

F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))

S tuples:

F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))

K tuples:

F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))

Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c3, c1, c2

(17) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))

S tuples:

F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))

K tuples:

F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0)))))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))

Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c3, c1, c2

(19) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(z1, c(z1), c(s(z0))) → c3(F(s(z0), s(z0), f(z0, s(c(z1)), c(s(z0))))) by

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))

S tuples:

F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))

K tuples:

F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0)))
F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))

Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c3, c1, c2

(21) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(z1, c(z1), c(s(z0))) → c3(F(s(z0), z1, s(z0))) by

F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))

S tuples:

F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))

K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))

Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c1, c2, c3

(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))

We considered the (Usable) Rules:

f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)

And the Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x₁, x₂, x₃)) = [4]x₁ + [4]x₃   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(f(x₁, x₂, x₃)) = x₃   
POL(s(x₁)) = [1] + x₁   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z0), c(z1)) → f(z1, z1, f(z1, z0, z1))
f(s(z0), z1, z2) → f(z0, s(c(z1)), c(z2))
f(c(z0), z0, z1) → c(z1)
g(z0, z1) → z0
g(z0, z1) → z1

Tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))
F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))

S tuples:

F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))

K tuples:

F(c(c(z1)), c(c(c(z1))), c(c(z1))) → c1(F(c(z1), c(c(z1)), c(z1)))
F(s(x1), x0, s(x1)) → c2(F(x1, s(c(x0)), c(s(x1))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), s(z1), f(z1, s(c(c(s(z1)))), c(s(z1)))))
F(c(s(z1)), c(c(s(z1))), c(s(z1))) → c3(F(s(z1), c(s(z1)), s(z1)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))

Defined Rule Symbols:

f, g

Defined Pair Symbols:

F

Compound Symbols:

c1, c2, c3

(25) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F(s(x1), s(x1), y0) → c2(F(x1, s(c(s(x1))), c(y0)))
F(s(z0), s(c(x1)), c(x2)) → c2(F(z0, s(c(s(c(x1)))), c(c(x2))))

Now S is empty

(26) BOUNDS(O(1), O(1))